package systemfnomabss


trait systemfnomabssSubstitution extends systemfnomabss.syntax.Substitution with TermSubstitutionProvider{ self: systemfnomabssSubstitution with systemfnomabss.AbstractSyntax =>

type partial = bruijnpart
type topsubst = bruijntopsubst


 object termintoterm_scope {
 implicit def LTermTakesLTermParam(self:LTerm):Substable[LTerm,LTerm] = new Substable[LTerm, LTerm] {
  //implicit def recursivecall(term:LTerm):Substable[LTerm,LTerm] = this(term) //implied, outer definition is visible
  implicit def abstakesterm(abs: \\[LTerm]):Substable[LTerm,\\[LTerm]] = (new AbsSubstTo[LTerm]).AbsIsSubstable(abs)
  // we 'import' the right implicit here => otherwise: in every case with an abs, explicitly apply the above to that abs
  
  def apply(self2:LTerm) = LTermTakesLTermParam(self2)
  def subst(sub: Name => Option[LTerm]): LTerm= self match {
    case b:BaseValue => b
    case If(cond,pos,neg) =>{
            val cond2 = cond subst sub;
            val pos2  = this(pos) subst sub;
            val neg2  = this(neg) subst sub;
            If(cond2,pos2,neg2) }
    case dis @ Var(n) => (sub(n).getOrElse[LTerm](dis))
    case App(fun,arg) => {
          val f2 = this(fun) subst(sub);
          val a2 = this(arg) subst(sub);
          App(f2, a2) }
    case Lam(ty,abs) => {
          val abs2 = abs subst(sub)
          Lam(ty, abs2 ) }
    case Let(impl,abs) => {
      val impl2 = this(impl).subst(sub)
      val abs2 = abs subst(sub)
      Let(impl2, abs2)
  }
    case TLam(abs) => {
          val abs2 = abs subst(sub)
          TLam( abs2 ) }
    case TApp(t,ty) => {
        val t2 = this(t) subst(sub)
        //ty2 <- AM.result(ty))//ty2 <- ty subst(sub)) 
        //yield TApp(t2, ty2)
        TApp(t2,ty) }
    case Pack(a,b,c) => {
      Pack(a,b.subst(sub),c)
    }
    case Unpack(impl, doubleabs) => {
      val impl2 = this(impl) .subst(sub);
      val doubleabs2 = doubleabs subst(sub)
      Unpack(impl2, doubleabs2)
  }
    case r@Record(fields) => Record(fields.map( {case (lbl,term) => (lbl, this(term).subst(sub)) }))
    case RecProj(rec, lbl) => RecProj(rec.subst(sub),lbl)
    case error => throw new Exception("substitution term into term match error on tree "+self)
    
  }
}
 
}


object typeintoterm_scope {
implicit def LTermTakesLTypeParam(self:LTerm):Substable[LType,LTerm] = new Substable[LType, LTerm] {
  
  implicit def abstakestype(abs: \\[LTerm]):Substable[LType,\\[LTerm]] = (new AbsSubstTo[LType]).AbsIsSubstable(abs) //declaration type suffices: new AbstSubstTo[LType].AbstIsSubstable not necessary
  // we 'import' the right implicit here => otherwise: in every case with an abs, explicitly apply the above to that abs
  def apply(self2:LTerm) = LTermTakesLTypeParam(self2)
  def subst(sub: Name => Option[LType]): LTerm= self match {
  case b:BaseValue => b
  case If(cond,pos,neg) =>  
    { val cond2 = cond subst sub; //TODO: obviously as long as the view is in scope, we can make this look like a normal map operation. create bounded functor instance?
      val pos2  = this(pos) subst sub;
      val neg2  = this(neg) subst sub;
      If(cond2,pos2,neg2) }
  case dis @ Var(n) => dis //(sub(n).getOrElse[LTerm](dis))
  case App(fun,arg) => 
    { val f2 = this(fun) subst(sub);
      val a2 = this(arg) subst(sub);
      App(f2, a2) }
  case Lam(ty,abs) => {
      val ty2 = ty.subst(sub);
      val abs2 = abs subst(sub);
      Lam(ty2, abs2 ) }
  case Let(impl,abs) => {
      val impl2 = this(impl).subst(sub)
      val abs2 = abs subst(sub)
      Let(impl2, abs2)
  }
  case TLam(abs) => {
      val abs2 = abs subst(sub)
      TLam( abs2 ) }
  case TApp(t,ty) => {
      val t2 = this(t) subst(sub);
      val ty2 = ty subst(sub);
      TApp(t2, ty2) }
  case Pack(a,b,c) => {
    Pack(a subst(sub),b subst(sub),c subst(sub))
  }
  case Unpack(impl, doubleabs) => {
      val impl2 = this(impl) .subst(sub);
      val doubleabs2 = doubleabs subst(sub)
      Unpack(impl2, doubleabs2)
  }
  case r@Record(fields) => Record(fields.map( {case (lbl,term) => (lbl, this(term).subst(sub)) }))
  case RecProj(rec, lbl) => RecProj(rec.subst(sub),lbl)
  case error => throw new Exception("substitution type into term match error on tree "+self)
  
}
}
}


implicit def LTypeTakesLTypeParam(self:LType):Substable[LType,LType] = new Substable[LType, LType] {
  def apply(self2:LType) = LTypeTakesLTypeParam(self2)
  def subst(sub: Name => Option[LType]): LType= self match {
    case b:BaseType => b
    case TyVar(n) => sub(n).getOrElse(self)
    case TyArr(t1, t2) => { val t1b = t1 subst sub;
                            val t2b = t2 subst sub;
                            TyArr(t1b,t2b) }
    case TyUniv(abs) => {
                            val abs2 = new AbsSubstTo[LType].AbsIsSubstable(abs) subst(sub);
                            TyUniv( abs2) }
    case TyExist(abs) => {
                            val abs2 = new AbsSubstTo[LType].AbsIsSubstable(abs) subst(sub);
                            TyExist( abs2) }
    case TyRecord(fields) => {
                            TyRecord(fields.map( {case (l,ty) => (l, ty subst (sub) )}))
    }
    case error => throw new Exception("substitution type into type match error on tree "+self)
  }
}

  

//type Term = LTerm
//type Type = LType
def substituteterm(v:Term)=new bruijnpart(v)
def substitutetype(v:Type)=new bruijnpart(v)
class bruijnpart(v:Node) extends termexamplepartial(v) {
  //def asTop() = new bruijntopsubst(v)
  def as(n:Name) = new bruijntopsubst(n,v) 
}

class bruijntopsubst(n:Name, v:Node) extends termexamplenamesubst(n,v) {
  import termintoterm_scope.{LTermTakesLTermParam}
  import typeintoterm_scope.{LTermTakesLTypeParam}
  
  def intoterm(term: Term)= (v,term) match {
    case (v:Type,t:Term)  => LTermTakesLTypeParam(t) subst {(name:Name)=> if (name == n) Some(v) else None}
    case (v:Term,t:Term)  => LTermTakesLTermParam(t) subst {(name:Name)=> if (name == n) Some(v) else None}
  }

  def intotype(ty: Type) = (v,ty) match {
    case (v:Type, ty:Type) => LTypeTakesLTypeParam(ty) subst {(name:Name)=> if (name == n) Some(v) else None}
    case (v:Term, ty:Type) => throw new Error("cannot form dependent type")
  }
}

}

object Test extends  systemfnomabssSubstitution with AbstractSyntax with Application {
  val x = Name("x")
  val y = Name("y")
  val z = Name("z")
  import termintoterm_scope.{LTermTakesLTermParam}
  import typeintoterm_scope.{LTermTakesLTypeParam}
  
  val subXtoZ = LTermTakesLTermParam(Lam(TyBool(),y\\Var(x))) subst (t => if(t == x) Some(Var(z)) else None)
  val subNop = LTermTakesLTermParam(Lam(TyBool(),x\\Var(x))) subst (t => if(t == x) Some(Var(z)) else None);
  val subType = LTermTakesLTypeParam((Lam(TyVar(y),z\\Var(x)))) subst (t => if(t==y) Some(TyBool()) else None);
  val subOnlyType =  LTypeTakesLTypeParam(TyVar(y)) . subst(t => if (t == y) Some(TyBool()) else None);
  val subOnlyType2 = LTypeTakesLTypeParam( TyUniv(x\\TyArr(TyBool(),TyVar(x))) ) . subst(t => if (t== x) Some(TyInt()) else None);
  val subOnlyType3 = LTypeTakesLTypeParam( TyUniv(x\\TyArr(TyBool(),TyVar(y))) ) . subst(t => if (t== y) Some(TyInt()) else None);
  val subOnlyType4 = LTypeTakesLTypeParam( TyUniv(x\\TyArr(TyBool(),TyVar(y))) ) . subst(t => if (t== y) Some(TyVar(x)) else None);
  val subTLamHit =  LTermTakesLTypeParam(TLam(x\\Lam(TyVar(x),y\\Var(y)))) subst( t => if (t == x) Some(TyInt()) else None);
  println( Lam(TyBool(),x\\Var(y)) == Lam (TyBool(),z\\Var(y)),
      Lam(TyBool(),x\\Var(y)) == Lam (TyBool(),y\\Var(x)),
      Lam(TyBool(),x\\Var(x)) == Lam (TyBool(),y\\Var(y)), subXtoZ, subNop,subType)
  println(subOnlyType  + (if (subOnlyType == TyBool()) "  OK" else "  should be TyBool()"))
  println(subOnlyType2 + (if (subOnlyType2 == TyUniv(x\\TyArr(TyBool(),TyVar(x)))) "  OK" else "  should be "+ TyUniv(x\\TyArr(TyBool(),TyVar(x))))) 
  println(subOnlyType3 + (if (subOnlyType3 == TyUniv(x\\TyArr(TyBool(),TyInt()))) "  OK" else "  should be "+ TyUniv(x\\TyArr(TyBool(),TyInt()))) )
  println(subOnlyType4 + (if (subOnlyType4 == TyUniv(x\\TyArr(TyBool(),TyVar(Name("x"))))) "  OK" else "  should be "+ TyUniv(x\\TyArr(TyBool(),TyVar(Name("x"))))) )//wrong, how to introduce new x? just compare toString?
  println(subTLamHit + (if (subTLamHit == TLam(x\\Lam(TyVar(x),y\\Var(y)))) "  OK" else "  should be "+  TLam(x\\Lam(TyVar(x),y\\Var(y)))))
  /*
  println((for(
      x <- gensym("x");
      y <- gensym("y");
      z <- gensym("z");
      subXtoZ <- LTermSubst(Lam(TyBool,y\\Var(x))) subst (t => if(t == x) Some(Var(z)) else None);
      subNop <- LTermSubst(Lam(TyBool,x\\Var(x))) subst (t => if(t == x) Some(Var(z)) else None);
      subType <- LTermTakesLTypeParam((Lam(TyVar(y),z\\Var(x)))) subst (t => if(t==y) Some(TyBool) else None);
      subOnlyType <- TyVar(y) . subst(t => if (t == y) Some(TyBool) else None);
      subTLamHit <- LTermTakesLTypeParam(TLam(x\\Lam(TyVar(x),y\\Var(y)))) subst( t => if (t == x) Some(TyInt) else None))
    yield (Lam(TyBool,x\\Var(y)) == Lam (TyBool,z\\Var(y)),
           Lam(TyBool,x\\Var(y)) == Lam (TyBool,y\\Var(x)),
           Lam(TyBool,x\\Var(x)) == Lam (TyBool,y\\Var(y)), subXtoZ, subNop,subType,
           subOnlyType,
           subTLamHit
           )).run) // prints "(true,false,true,Lam(y$0\\Var(z$2)),Lam(x$0\\Var(x$0)))"
   */
}
